Nuprl Definition : combine-ecl-tuples2 0,22

combine-ecl-tuples2(A;B;f;g)
== let Ta,ksa,ia,ga,ha,aa,ea = A in 
== let Tb,ksb,ib,gb,hb,ab,eb = B in 
== <(TaTb(+Unit))
== ,(ksa @ ksb)
== ,<ia,ib,inr()>
== ,(k',s,v,x. let sa = if deq-member(KindDeq;k';ksa) ga(k',s,v,1of(x)) else 1of(x) fi in 
== ,(k',s,v,xlet sb = if deq-member(KindDeq;k';ksb) gb(k',s,v,1of(2of(x)))
== ,(k',s,v,x. let sb = else 1of(2of(x)) fi in 
== ,(k',s,v,x<sa,sb,combine-halt-info(ea;eb;m.ha(m,sa);m.hb(m,sb);2of(2of(x)))>)
== ,(n,xf(2of(2of(x)),m.ha(m,1of(x)),m.hb(m,1of(2of(x))),n))
== ,(n,k',s,v,xg
== ,(n,k',s,v,x(ha(0,1of(x))
== ,(n,k',s,v,x,hb(0,1of(2of(x)))
== ,(n,k',s,v,x,reduce(m,bha(m,1of(x))  b;false;ea)
== ,(n,k',s,v,x,reduce(m,bhb(m,1of(2of(x)))  b;false;eb)
== ,(n,k',s,v,x,if deq-member(KindDeq;k';ksa) aa(n,k',s,v,1of(x)) else false fi
== ,(n,k',s,v,x,if deq-member(KindDeq;k';ksb) ab(n,k',s,v,1of(2of(x))) else false fi))
== ,merge(ea;eb)> 
latex


Definitionscombine-ecl-tuples2(A;B;f;g), let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), , Unit, as @ bs, , let x = a in b(x), combine-halt-info(ea;eb;f;g;x), reduce(f;k;as), p  q, if b t else f fi, deq-member(eq;x;L), KindDeq, 1of(t), 2of(t), false, merge(as;bs)
FDL editor aliasescombine-ecl-tuples2

origin